fin1a2lem13 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin1a2lem13		Structured version Visualization version GIF version

Theorem fin1a2lem13 9446

Description: Lemma for fin1a2 9449. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

**Assertion**
Ref	Expression
fin1a2lem13	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ Fin^II)

Proof of Theorem fin1a2lem13 Dummy variables 𝑒 𝑓 𝑔 ℎ 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 479	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (𝐵 ∖ 𝐶) ∈ Fin^II)
2		simpll1 1255	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐴 ⊆ 𝒫 𝐵)
3		ssel2 3739	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵)
4	3	elpwid 4314	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵)
5	4	ssdifd 3889	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
6		sseq1 3767	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)))
7	5, 6	syl5ibrcom 237	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
8	7	rexlimdva 3169	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
9		vex 3343	. . . . . . 7 ⊢ 𝑓 ∈ V
10		eqid 2760	. . . . . . . 8 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))
11	10	elrnmpt 5527	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)))
12	9, 11	ax-mp 5	. . . . . 6 ⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))
13		selpw 4309	. . . . . 6 ⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶))
14	8, 12, 13	3imtr4g 285	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶)))
15	14	ssrdv 3750	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
16	2, 15	syl 17	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
17		simplrr 820	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐶 ∈ 𝐴)
18		difid 4091	. . . . . . 7 ⊢ (𝐶 ∖ 𝐶) = ∅
19	18	eqcomi 2769	. . . . . 6 ⊢ ∅ = (𝐶 ∖ 𝐶)
20		difeq1 3864	. . . . . . . 8 ⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶))
21	20	eqeq2d 2770	. . . . . . 7 ⊢ (𝑔 = 𝐶 → (∅ = (𝑔 ∖ 𝐶) ↔ ∅ = (𝐶 ∖ 𝐶)))
22	21	rspcev 3449	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
23	19, 22	mpan2 709	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
24		0ex 4942	. . . . . 6 ⊢ ∅ ∈ V
25	10	elrnmpt 5527	. . . . . 6 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)))
26	24, 25	ax-mp 5	. . . . 5 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
27	23, 26	sylibr 224	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
28		ne0i 4064	. . . 4 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
29	17, 27, 28	3syl 18	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
30		simpll2 1257	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → [⊊] Or 𝐴)
31		vex 3343	. . . . . . . 8 ⊢ 𝑥 ∈ V
32	10	elrnmpt 5527	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)))
33	31, 32	ax-mp 5	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))
34		difeq1 3864	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶))
35	34	eqeq2d 2770	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶)))
36	35	cbvrexv 3311	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶))
37		sorpssi 7109	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒))
38		ssdif 3888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))
39		ssdif 3888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))
40	38, 39	orim12i 539	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
41	37, 40	syl 17	. . . . . . . . . . . . . . 15 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
42		sseq2 3768	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)))
43		sseq1 3767	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
44	42, 43	orbi12d 748	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))))
45	41, 44	syl5ibrcom 237	. . . . . . . . . . . . . 14 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
46	45	expr 644	. . . . . . . . . . . . 13 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))))
47	46	rexlimdv 3168	. . . . . . . . . . . 12 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
48	12, 47	syl5bi 232	. . . . . . . . . . 11 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
49	48	ralrimiv 3103	. . . . . . . . . 10 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
50		sseq1 3767	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓))
51		sseq2 3768	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
52	50, 51	orbi12d 748	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
53	52	ralbidv 3124	. . . . . . . . . 10 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
54	49, 53	syl5ibrcom 237	. . . . . . . . 9 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
55	54	rexlimdva 3169	. . . . . . . 8 ⊢ ( [⊊] Or 𝐴 → (∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
56	36, 55	syl5bi 232	. . . . . . 7 ⊢ ( [⊊] Or 𝐴 → (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
57	33, 56	syl5bi 232	. . . . . 6 ⊢ ( [⊊] Or 𝐴 → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
58	57	ralrimiv 3103	. . . . 5 ⊢ ( [⊊] Or 𝐴 → ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))
59		sorpss 7108	. . . . 5 ⊢ ( [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))
60	58, 59	sylibr 224	. . . 4 ⊢ ( [⊊] Or 𝐴 → [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
61	30, 60	syl 17	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
62		fin2i 9329	. . 3 ⊢ ((((𝐵 ∖ 𝐶) ∈ Fin^II ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
63	1, 16, 29, 61, 62	syl22anc 1478	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
64		simpll3 1259	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ¬ ∪ 𝐴 ∈ 𝐴)
65		difeq1 3864	. . . . . . 7 ⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶))
66	65	cbvmptv 4902	. . . . . 6 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶))
67	66	elrnmpt 5527	. . . . 5 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)))
68	67	ibi 256	. . . 4 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
69		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)
70		difeq1 3864	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶))
71	70	eqeq2d 2770	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → ((ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)))
72	71	rspcev 3449	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
73	69, 72	mpan2 709	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
74	73	adantl 473	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
75		vex 3343	. . . . . . . . . . . . . . 15 ⊢ ℎ ∈ V
76		difexg 4960	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V)
77	10	elrnmpt 5527	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)))
78	75, 76, 77	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
79	74, 78	sylibr 224	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
80		elssuni 4619	. . . . . . . . . . . . 13 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
81	79, 80	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
82		simplr 809	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
83	81, 82	sseqtrd 3782	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
84	83	adantll 752	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
85		unss2 3927	. . . . . . . . . . 11 ⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)))
86		uncom 3900	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶)
87		undif1 4187	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶)
88	86, 87	eqtri 2782	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)
89	88	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶))
90	64	ad2antrr 764	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪ 𝐴 ∈ 𝐴)
91	17	ad2antrr 764	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴)
92		simplrr 820	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
93		eqeq1 2764	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅))
94		simpllr 817	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
95		ssdif0 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅)
96	95	biimpi 206	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅)
97	96	ad2antlr 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅)
98	94, 97	eqtrd 2794	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅)
99		uni0c 4616	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
100	98, 99	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
101		eqid 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)
102		difeq1 3864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶))
103	102	eqeq2d 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = 𝑥 → ((𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶) ↔ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)))
104	103	rspcev 3449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
105	101, 104	mpan2 709	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
106		difexg 4960	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V)
107	10	elrnmpt 5527	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)))
108	31, 106, 107	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
109	105, 108	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
110	109	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
111	93, 100, 110	rspcdva 3455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅)
112		ssdif0 4085	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅)
113	111, 112	sylibr 224	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶)
114	113	ralrimiva 3104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
115		unissb 4621	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝐴 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
116	114, 115	sylibr 224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶)
117		elssuni 4619	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴)
118	117	ad2antrr 764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴)
119	116, 118	eqssd 3761	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶)
120		simpll 807	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴)
121	119, 120	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴)
122	121	ex 449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
123	91, 92, 122	syl2anc 696	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
124	90, 123	mtod 189	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶)
125	30	ad2antrr 764	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴)
126		simplrl 819	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴)
127		sorpssi 7109	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
128	125, 126, 91, 127	syl12anc 1475	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
129		orel1 396	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓))
130	124, 128, 129	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓)
131		undif 4193	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
132	130, 131	sylib 208	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
133	89, 132	sseq12d 3775	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓))
134		ssun1 3919	. . . . . . . . . . . . 13 ⊢ ℎ ⊆ (ℎ ∪ 𝐶)
135		sstr 3752	. . . . . . . . . . . . 13 ⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓)
136	134, 135	mpan 708	. . . . . . . . . . . 12 ⊢ ((ℎ ∪ 𝐶) ⊆ 𝑓 → ℎ ⊆ 𝑓)
137	133, 136	syl6bi 243	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) → ℎ ⊆ 𝑓))
138	85, 137	syl5 34	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → ℎ ⊆ 𝑓))
139	84, 138	mpd 15	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ℎ ⊆ 𝑓)
140	139	ralrimiva 3104	. . . . . . . 8 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
141		unissb 4621	. . . . . . . 8 ⊢ (∪ 𝐴 ⊆ 𝑓 ↔ ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
142	140, 141	sylibr 224	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ⊆ 𝑓)
143		elssuni 4619	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴)
144	143	ad2antrl 766	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴)
145	142, 144	eqssd 3761	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 = 𝑓)
146		simprl 811	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴)
147	145, 146	eqeltrd 2839	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ∈ 𝐴)
148	147	rexlimdvaa 3170	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶) → ∪ 𝐴 ∈ 𝐴))
149	68, 148	syl5 34	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∪ 𝐴 ∈ 𝐴))
150	64, 149	mtod 189	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ¬ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
151	63, 150	pm2.65da 601	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ Fin^II)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∨ wo 382 ∧ wa 383 ∧ w3a 1072 = wceq 1632 ∈ wcel 2139 ≠ wne 2932 ∀wral 3050 ∃wrex 3051 Vcvv 3340 ∖ cdif 3712 ∪ cun 3713 ⊆ wss 3715 ∅c0 4058 𝒫 cpw 4302 ∪ cuni 4588 ↦ cmpt 4881 Or wor 5186 ran crn 5267 [⊊] crpss 7102 Fincfn 8123 Fin^IIcfin2 9313

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-mpt 4882 df-po 5187 df-so 5188 df-xp 5272 df-rel 5273 df-cnv 5274 df-dm 5276 df-rn 5277 df-rpss 7103 df-fin2 9320

This theorem is referenced by: fin1a2s 9448

W3C validator