Theorem fnejoin2 11592

Description: Join of equivalence classes under the fineness relation-part two.

Assertion

Ref	Expression
fnejoin2	⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → ∀v((X = ∪v ⋀ ∀x ∈ S xFnev) → if(S = ∅, {X}, ∪S)Fnev))

Distinct variable groups:   x,v,y,A   v,S,x,y   v,X,x,y

Proof of Theorem fnejoin2

Step	Hyp	Ref	Expression
1		iftrue 2420	. . . . . 6 ⊢ (S = ∅ → if(S = ∅, {X}, ∪S) = {X})
2	1	breq1d 2702	. . . . 5 ⊢ (S = ∅ → ( if(S = ∅, {X}, ∪S)Fnev ↔ {X}Fnev))
3		unisng 2585	. . . . . . . . . 10 ⊢ (X ∈ A → ∪{X} = X)
4	3	adantr 389	. . . . . . . . 9 ⊢ ((X ∈ A ⋀ X = ∪v) → ∪{X} = X)
5		pm3.27 321	. . . . . . . . 9 ⊢ ((X ∈ A ⋀ X = ∪v) → X = ∪v)
6	4, 5	eqtrd 1550	. . . . . . . 8 ⊢ ((X ∈ A ⋀ X = ∪v) → ∪{X} = ∪v)
7		pm3.27 321	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ z ⋀ z ∈ v) → z ∈ v)
8		pm3.26 317	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ z ⋀ z ∈ v) → x ∈ z)
9		elssuni 2593	. . . . . . . . . . . . . . . . . 18 ⊢ (z ∈ v → z ⊆ ∪v)
10	9	adantl 388	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ z ⋀ z ∈ v) → z ⊆ ∪v)
11	7, 8, 10	jca32 11341	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ z ⋀ z ∈ v) → (z ∈ v ⋀ (x ∈ z ⋀ z ⊆ ∪v)))
12	11	19.22i 1076	. . . . . . . . . . . . . . 15 ⊢ (∃z(x ∈ z ⋀ z ∈ v) → ∃z(z ∈ v ⋀ (x ∈ z ⋀ z ⊆ ∪v)))
13		eluni 2572	. . . . . . . . . . . . . . 15 ⊢ (x ∈ ∪v ↔ ∃z(x ∈ z ⋀ z ∈ v))
14		df-rex 1696	. . . . . . . . . . . . . . 15 ⊢ (∃z ∈ v (x ∈ z ⋀ z ⊆ ∪v) ↔ ∃z(z ∈ v ⋀ (x ∈ z ⋀ z ⊆ ∪v)))
15	12, 13, 14	3imtr4i 217	. . . . . . . . . . . . . 14 ⊢ (x ∈ ∪v → ∃z ∈ v (x ∈ z ⋀ z ⊆ ∪v))
16		eleq2 1578	. . . . . . . . . . . . . . 15 ⊢ (X = ∪v → (x ∈ X ↔ x ∈ ∪v))
17		sseq2 2135	. . . . . . . . . . . . . . . . 17 ⊢ (X = ∪v → (z ⊆ X ↔ z ⊆ ∪v))
18	17	anbi2d 619	. . . . . . . . . . . . . . . 16 ⊢ (X = ∪v → ((x ∈ z ⋀ z ⊆ X) ↔ (x ∈ z ⋀ z ⊆ ∪v)))
19	18	rexbidv 1710	. . . . . . . . . . . . . . 15 ⊢ (X = ∪v → (∃z ∈ v (x ∈ z ⋀ z ⊆ X) ↔ ∃z ∈ v (x ∈ z ⋀ z ⊆ ∪v)))
20	16, 19	imbi12d 629	. . . . . . . . . . . . . 14 ⊢ (X = ∪v → ((x ∈ X → ∃z ∈ v (x ∈ z ⋀ z ⊆ X)) ↔ (x ∈ ∪v → ∃z ∈ v (x ∈ z ⋀ z ⊆ ∪v))))
21	15, 20	mpbiri 192	. . . . . . . . . . . . 13 ⊢ (X = ∪v → (x ∈ X → ∃z ∈ v (x ∈ z ⋀ z ⊆ X)))
22	21	ad2antlr 405	. . . . . . . . . . . 12 ⊢ (((X ∈ A ⋀ X = ∪v) ⋀ y = X) → (x ∈ X → ∃z ∈ v (x ∈ z ⋀ z ⊆ X)))
23		eleq2 1578	. . . . . . . . . . . . 13 ⊢ (y = X → (x ∈ y ↔ x ∈ X))
24	23	adantl 388	. . . . . . . . . . . 12 ⊢ (((X ∈ A ⋀ X = ∪v) ⋀ y = X) → (x ∈ y ↔ x ∈ X))
25		sseq2 2135	. . . . . . . . . . . . . . 15 ⊢ (y = X → (z ⊆ y ↔ z ⊆ X))
26	25	anbi2d 619	. . . . . . . . . . . . . 14 ⊢ (y = X → ((x ∈ z ⋀ z ⊆ y) ↔ (x ∈ z ⋀ z ⊆ X)))
27	26	rexbidv 1710	. . . . . . . . . . . . 13 ⊢ (y = X → (∃z ∈ v (x ∈ z ⋀ z ⊆ y) ↔ ∃z ∈ v (x ∈ z ⋀ z ⊆ X)))
28	27	adantl 388	. . . . . . . . . . . 12 ⊢ (((X ∈ A ⋀ X = ∪v) ⋀ y = X) → (∃z ∈ v (x ∈ z ⋀ z ⊆ y) ↔ ∃z ∈ v (x ∈ z ⋀ z ⊆ X)))
29	22, 24, 28	3imtr4d 546	. . . . . . . . . . 11 ⊢ (((X ∈ A ⋀ X = ∪v) ⋀ y = X) → (x ∈ y → ∃z ∈ v (x ∈ z ⋀ z ⊆ y)))
30	29	expimpd 373	. . . . . . . . . 10 ⊢ ((X ∈ A ⋀ X = ∪v) → ((y = X ⋀ x ∈ y) → ∃z ∈ v (x ∈ z ⋀ z ⊆ y)))
31		elsni 2493	. . . . . . . . . 10 ⊢ (y ∈ {X} → y = X)
32	30, 31	sylani 466	. . . . . . . . 9 ⊢ ((X ∈ A ⋀ X = ∪v) → ((y ∈ {X} ⋀ x ∈ y) → ∃z ∈ v (x ∈ z ⋀ z ⊆ y)))
33	32	r19.21aivv 1766	. . . . . . . 8 ⊢ ((X ∈ A ⋀ X = ∪v) → ∀y ∈ {X}∀x ∈ y ∃z ∈ v (x ∈ z ⋀ z ⊆ y))
34	6, 33	jca 286	. . . . . . 7 ⊢ ((X ∈ A ⋀ X = ∪v) → (∪{X} = ∪v ⋀ ∀y ∈ {X}∀x ∈ y ∃z ∈ v (x ∈ z ⋀ z ⊆ y)))
35		visset 1859	. . . . . . . 8 ⊢ v ∈ V
36		eqid 1518	. . . . . . . . 9 ⊢ ∪{X} = ∪{X}
37		eqid 1518	. . . . . . . . 9 ⊢ ∪v = ∪v
38	36, 37	isfne2 11542	. . . . . . . 8 ⊢ (v ∈ V → ({X}Fnev ↔ (∪{X} = ∪v ⋀ ∀y ∈ {X}∀x ∈ y ∃z ∈ v (x ∈ z ⋀ z ⊆ y))))
39	35, 38	ax-mp 7	. . . . . . 7 ⊢ ({X}Fnev ↔ (∪{X} = ∪v ⋀ ∀y ∈ {X}∀x ∈ y ∃z ∈ v (x ∈ z ⋀ z ⊆ y)))
40	34, 39	sylibr 198	. . . . . 6 ⊢ ((X ∈ A ⋀ X = ∪v) → {X}Fnev)
41	40	ad2ant2r 409	. . . . 5 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) → {X}Fnev)
42	2, 41	syl5cbir 209	. . . 4 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) → (S = ∅ → if(S = ∅, {X}, ∪S)Fnev))
43		ssel 2115	. . . . . . . . . . . . . . . . . . 19 ⊢ (S ⊆ {y∣X = ∪y} → (k ∈ S → k ∈ {y∣X = ∪y}))
44		elssuni 2593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (t ∈ k → t ⊆ ∪k)
45	44	adantl 388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((X = ∪k ⋀ t ∈ k) → t ⊆ ∪k)
46		pm3.26 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((X = ∪k ⋀ t ∈ k) → X = ∪k)
47	45, 46	sseqtr4d 2150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((X = ∪k ⋀ t ∈ k) → t ⊆ X)
48	47	ex 371	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (X = ∪k → (t ∈ k → t ⊆ X))
49	48	a1i 8	. . . . . . . . . . . . . . . . . . . 20 ⊢ (X ∈ A → (X = ∪k → (t ∈ k → t ⊆ X)))
50		visset 1859	. . . . . . . . . . . . . . . . . . . . 21 ⊢ k ∈ V
51		unieq 2576	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (y = k → ∪y = ∪k)
52	51	eqeq2d 1529	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = k → (X = ∪y ↔ X = ∪k))
53	50, 52	elab 1943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (k ∈ {y∣X = ∪y} ↔ X = ∪k)
54	49, 53	syl5ib 204	. . . . . . . . . . . . . . . . . . 19 ⊢ (X ∈ A → (k ∈ {y∣X = ∪y} → (t ∈ k → t ⊆ X)))
55	43, 54	syl9r 58	. . . . . . . . . . . . . . . . . 18 ⊢ (X ∈ A → (S ⊆ {y∣X = ∪y} → (k ∈ S → (t ∈ k → t ⊆ X))))
56	55	com34 36	. . . . . . . . . . . . . . . . 17 ⊢ (X ∈ A → (S ⊆ {y∣X = ∪y} → (t ∈ k → (k ∈ S → t ⊆ X))))
57	56	imp4b 363	. . . . . . . . . . . . . . . 16 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → ((t ∈ k ⋀ k ∈ S) → t ⊆ X))
58	57	adantr 389	. . . . . . . . . . . . . . 15 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → ((t ∈ k ⋀ k ∈ S) → t ⊆ X))
59	58	19.23adv 1251	. . . . . . . . . . . . . 14 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → (∃k(t ∈ k ⋀ k ∈ S) → t ⊆ X))
60		eluni 2572	. . . . . . . . . . . . . 14 ⊢ (t ∈ ∪S ↔ ∃k(t ∈ k ⋀ k ∈ S))
61	59, 60	syl5ib 204	. . . . . . . . . . . . 13 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → (t ∈ ∪S → t ⊆ X))
62	61	r19.21aiv 1759	. . . . . . . . . . . 12 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → ∀t ∈ ∪St ⊆ X)
63		unissb 2595	. . . . . . . . . . . 12 ⊢ (∪∪S ⊆ X ↔ ∀t ∈ ∪St ⊆ X)
64	62, 63	sylibr 198	. . . . . . . . . . 11 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → ∪∪S ⊆ X)
65		ssel 2115	. . . . . . . . . . . . . . . . . . 19 ⊢ (S ⊆ {y∣X = ∪y} → (s ∈ S → s ∈ {y∣X = ∪y}))
66	65	com12 11	. . . . . . . . . . . . . . . . . 18 ⊢ (s ∈ S → (S ⊆ {y∣X = ∪y} → s ∈ {y∣X = ∪y}))
67		eleq2 1578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (X = ∪s → (t ∈ X ↔ t ∈ ∪s))
68	67	biimpd 151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (X = ∪s → (t ∈ X → t ∈ ∪s))
69		elssuni 2593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (s ∈ S → s ⊆ ∪S)
70		uniss 2588	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (s ⊆ ∪S → ∪s ⊆ ∪∪S)
71	69, 70	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (s ∈ S → ∪s ⊆ ∪∪S)
72	71	sseld 2119	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (s ∈ S → (t ∈ ∪s → t ∈ ∪∪S))
73	68, 72	syl9r 58	. . . . . . . . . . . . . . . . . . . 20 ⊢ (s ∈ S → (X = ∪s → (t ∈ X → t ∈ ∪∪S)))
74	73	a1dd 42	. . . . . . . . . . . . . . . . . . 19 ⊢ (s ∈ S → (X = ∪s → (X ∈ A → (t ∈ X → t ∈ ∪∪S))))
75		visset 1859	. . . . . . . . . . . . . . . . . . . 20 ⊢ s ∈ V
76		unieq 2576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y = s → ∪y = ∪s)
77	76	eqeq2d 1529	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y = s → (X = ∪y ↔ X = ∪s))
78	75, 77	elab 1943	. . . . . . . . . . . . . . . . . . 19 ⊢ (s ∈ {y∣X = ∪y} ↔ X = ∪s)
79	74, 78	syl5ib 204	. . . . . . . . . . . . . . . . . 18 ⊢ (s ∈ S → (s ∈ {y∣X = ∪y} → (X ∈ A → (t ∈ X → t ∈ ∪∪S))))
80	66, 79	syld 27	. . . . . . . . . . . . . . . . 17 ⊢ (s ∈ S → (S ⊆ {y∣X = ∪y} → (X ∈ A → (t ∈ X → t ∈ ∪∪S))))
81	80	com13 33	. . . . . . . . . . . . . . . 16 ⊢ (X ∈ A → (S ⊆ {y∣X = ∪y} → (s ∈ S → (t ∈ X → t ∈ ∪∪S))))
82	81	imp 348	. . . . . . . . . . . . . . 15 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (s ∈ S → (t ∈ X → t ∈ ∪∪S)))
83	82	19.23adv 1251	. . . . . . . . . . . . . 14 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (∃s s ∈ S → (t ∈ X → t ∈ ∪∪S)))
84	83	imp 348	. . . . . . . . . . . . 13 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ∃s s ∈ S) → (t ∈ X → t ∈ ∪∪S))
85		neq0 2342	. . . . . . . . . . . . 13 ⊢ (¬ S = ∅ ↔ ∃s s ∈ S)
86	84, 85	sylan2b 454	. . . . . . . . . . . 12 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → (t ∈ X → t ∈ ∪∪S))
87	86	ssrdv 2122	. . . . . . . . . . 11 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → X ⊆ ∪∪S)
88	64, 87	eqssd 2131	. . . . . . . . . 10 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ ¬ S = ∅) → ∪∪S = X)
89	88	adantlr 393	. . . . . . . . 9 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ∪∪S = X)
90		simplrl 11364	. . . . . . . . 9 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → X = ∪v)
91	89, 90	eqtrd 1550	. . . . . . . 8 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ∪∪S = ∪v)
92		breq1 2695	. . . . . . . . . . . . . . . . . 18 ⊢ (x = s → (xFnev ↔ sFnev))
93	92	rcla4v 1919	. . . . . . . . . . . . . . . . 17 ⊢ (s ∈ S → (∀x ∈ S xFnev → sFnev))
94		fnessex 11545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((v ∈ V ⋀ sFnev ⋀ z ∈ s) ⋀ w ∈ z) → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))
95	94	3exp1 855	. . . . . . . . . . . . . . . . . . . 20 ⊢ (v ∈ V → (sFnev → (z ∈ s → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))))
96	35, 95	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 ⊢ (sFnev → (z ∈ s → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))
97	96	a1dd 42	. . . . . . . . . . . . . . . . . 18 ⊢ (sFnev → (z ∈ s → ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))))
98	97	a1i24 11336	. . . . . . . . . . . . . . . . 17 ⊢ (sFnev → (X = ∪v → (z ∈ s → (¬ S = ∅ → ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))))))
99	93, 98	syl6 22	. . . . . . . . . . . . . . . 16 ⊢ (s ∈ S → (∀x ∈ S xFnev → (X = ∪v → (z ∈ s → (¬ S = ∅ → ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))))))
100	99	com24 37	. . . . . . . . . . . . . . 15 ⊢ (s ∈ S → (z ∈ s → (X = ∪v → (∀x ∈ S xFnev → (¬ S = ∅ → ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))))))
101	100	impcom 349	. . . . . . . . . . . . . 14 ⊢ ((z ∈ s ⋀ s ∈ S) → (X = ∪v → (∀x ∈ S xFnev → (¬ S = ∅ → ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))))))
102	101	com15 11328	. . . . . . . . . . . . 13 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → (X = ∪v → (∀x ∈ S xFnev → (¬ S = ∅ → ((z ∈ s ⋀ s ∈ S) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))))))
103	102	imp42 367	. . . . . . . . . . . 12 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ((z ∈ s ⋀ s ∈ S) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))
104	103	19.23adv 1251	. . . . . . . . . . 11 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → (∃s(z ∈ s ⋀ s ∈ S) → (w ∈ z → ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))
105	104	imp3a 359	. . . . . . . . . 10 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ((∃s(z ∈ s ⋀ s ∈ S) ⋀ w ∈ z) → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))
106		eluni 2572	. . . . . . . . . . 11 ⊢ (z ∈ ∪S ↔ ∃s(z ∈ s ⋀ s ∈ S))
107	106	biimpi 149	. . . . . . . . . 10 ⊢ (z ∈ ∪S → ∃s(z ∈ s ⋀ s ∈ S))
108	105, 107	sylani 466	. . . . . . . . 9 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ((z ∈ ∪S ⋀ w ∈ z) → ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))
109	108	r19.21aivv 1766	. . . . . . . 8 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ∀z ∈ ∪S∀w ∈ z ∃t ∈ v (w ∈ t ⋀ t ⊆ z))
110	91, 109	jca 286	. . . . . . 7 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → (∪∪S = ∪v ⋀ ∀z ∈ ∪S∀w ∈ z ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))
111		eqid 1518	. . . . . . . . 9 ⊢ ∪∪S = ∪∪S
112	111, 37	isfne2 11542	. . . . . . . 8 ⊢ (v ∈ V → (∪SFnev ↔ (∪∪S = ∪v ⋀ ∀z ∈ ∪S∀w ∈ z ∃t ∈ v (w ∈ t ⋀ t ⊆ z))))
113	35, 112	ax-mp 7	. . . . . . 7 ⊢ (∪SFnev ↔ (∪∪S = ∪v ⋀ ∀z ∈ ∪S∀w ∈ z ∃t ∈ v (w ∈ t ⋀ t ⊆ z)))
114	110, 113	sylibr 198	. . . . . 6 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ∪SFnev)
115		iffalse 2421	. . . . . . . 8 ⊢ (¬ S = ∅ → if(S = ∅, {X}, ∪S) = ∪S)
116	115	breq1d 2702	. . . . . . 7 ⊢ (¬ S = ∅ → ( if(S = ∅, {X}, ∪S)Fnev ↔ ∪SFnev))
117	116	adantl 388	. . . . . 6 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → ( if(S = ∅, {X}, ∪S)Fnev ↔ ∪SFnev))
118	114, 117	mpbird 194	. . . . 5 ⊢ ((((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) ⋀ ¬ S = ∅) → if(S = ∅, {X}, ∪S)Fnev)
119	118	ex 371	. . . 4 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) → (¬ S = ∅ → if(S = ∅, {X}, ∪S)Fnev))
120	42, 119	pm2.61d 125	. . 3 ⊢ (((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) ⋀ (X = ∪v ⋀ ∀x ∈ S xFnev)) → if(S = ∅, {X}, ∪S)Fnev)
121	120	ex 371	. 2 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → ((X = ∪v ⋀ ∀x ∈ S xFnev) → if(S = ∅, {X}, ∪S)Fnev))
122	121	19.21aiv 1324	1 ⊢ ((X ∈ A ⋀ S ⊆ {y∣X = ∪y}) → ∀v((X = ∪v ⋀ ∀x ∈ S xFnev) → if(S = ∅, {X}, ∪S)Fnev))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 144   ⋀ wa 221  ∀wal 990   = wceq 992   ∈ wcel 994  ∃wex 1016  {cab 1505  ∀wral 1691  ∃wrex 1692  Vcvv 1857   ⊆ wss 2099  ∅c0 2332   ifcif 2415  {csn 2467  ∪cuni 2569   class class class wbr 2692  Fnecfne 11518

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-rel 3266  df-fne 11524

Copyright terms: Public domain