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 10099

Description: Lemma for fin1a2 10102. (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 484	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (𝐵 ∖ 𝐶) ∈ Fin^II)
2		simpll1 1210	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐴 ⊆ 𝒫 𝐵)
3		ssel2 3912	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵)
4	3	elpwid 4541	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵)
5	4	ssdifd 4071	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
6		sseq1 3942	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)))
7	5, 6	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
8	7	rexlimdva 3212	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
9		eqid 2738	. . . . . . . 8 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))
10	9	elrnmpt 5854	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)))
11	10	elv 3428	. . . . . 6 ⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))
12		velpw 4535	. . . . . 6 ⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶))
13	8, 11, 12	3imtr4g 295	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶)))
14	13	ssrdv 3923	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
15	2, 14	syl 17	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
16		simplrr 774	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐶 ∈ 𝐴)
17		difid 4301	. . . . . . 7 ⊢ (𝐶 ∖ 𝐶) = ∅
18	17	eqcomi 2747	. . . . . 6 ⊢ ∅ = (𝐶 ∖ 𝐶)
19		difeq1 4046	. . . . . . 7 ⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶))
20	19	rspceeqv 3567	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
21	18, 20	mpan2 687	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
22		0ex 5226	. . . . . 6 ⊢ ∅ ∈ V
23	9	elrnmpt 5854	. . . . . 6 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)))
24	22, 23	ax-mp 5	. . . . 5 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
25	21, 24	sylibr 233	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
26		ne0i 4265	. . . 4 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
27	16, 25, 26	3syl 18	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
28		simpll2 1211	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → [⊊] Or 𝐴)
29	9	elrnmpt 5854	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)))
30	29	elv 3428	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))
31		difeq1 4046	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶))
32	31	eqeq2d 2749	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶)))
33	32	cbvrexvw 3373	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶))
34		sorpssi 7560	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒))
35		ssdif 4070	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))
36		ssdif 4070	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))
37	35, 36	orim12i 905	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
38	34, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
39		sseq2 3943	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)))
40		sseq1 3942	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
41	39, 40	orbi12d 915	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))))
42	38, 41	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
43	42	expr 456	. . . . . . . . . . . . 13 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))))
44	43	rexlimdv 3211	. . . . . . . . . . . 12 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
45	11, 44	syl5bi 241	. . . . . . . . . . 11 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
46	45	ralrimiv 3106	. . . . . . . . . 10 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
47		sseq1 3942	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓))
48		sseq2 3943	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
49	47, 48	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
50	49	ralbidv 3120	. . . . . . . . . 10 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
51	46, 50	syl5ibrcom 246	. . . . . . . . 9 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
52	51	rexlimdva 3212	. . . . . . . 8 ⊢ ( [⊊] Or 𝐴 → (∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
53	33, 52	syl5bi 241	. . . . . . 7 ⊢ ( [⊊] Or 𝐴 → (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
54	30, 53	syl5bi 241	. . . . . 6 ⊢ ( [⊊] Or 𝐴 → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
55	54	ralrimiv 3106	. . . . 5 ⊢ ( [⊊] Or 𝐴 → ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))
56		sorpss 7559	. . . . 5 ⊢ ( [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))
57	55, 56	sylibr 233	. . . 4 ⊢ ( [⊊] Or 𝐴 → [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
58	28, 57	syl 17	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
59		fin2i 9982	. . 3 ⊢ ((((𝐵 ∖ 𝐶) ∈ Fin^II ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
60	1, 15, 27, 58, 59	syl22anc 835	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
61		simpll3 1212	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ¬ ∪ 𝐴 ∈ 𝐴)
62		difeq1 4046	. . . . . . 7 ⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶))
63	62	cbvmptv 5183	. . . . . 6 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶))
64	63	elrnmpt 5854	. . . . 5 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)))
65	64	ibi 266	. . . 4 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
66		eqid 2738	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)
67		difeq1 4046	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶))
68	67	rspceeqv 3567	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
69	66, 68	mpan2 687	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
70	69	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
71		vex 3426	. . . . . . . . . . . . . . 15 ⊢ ℎ ∈ V
72		difexg 5246	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V)
73	9	elrnmpt 5854	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)))
74	71, 72, 73	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
75	70, 74	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
76		elssuni 4868	. . . . . . . . . . . . 13 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
77	75, 76	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
78		simplr 765	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
79	77, 78	sseqtrd 3957	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
80	79	adantll 710	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
81		unss2 4111	. . . . . . . . . . 11 ⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)))
82		uncom 4083	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶)
83		undif1 4406	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶)
84	82, 83	eqtri 2766	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)
85	84	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶))
86	61	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪ 𝐴 ∈ 𝐴)
87	16	ad2antrr 722	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴)
88		simplrr 774	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
89		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅))
90		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
91		ssdif0 4294	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅)
92	91	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅)
93	92	ad2antlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅)
94	90, 93	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅)
95		uni0c 4865	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
96	94, 95	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
97		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)
98		difeq1 4046	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶))
99	98	rspceeqv 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
100	97, 99	mpan2 687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
101		vex 3426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑥 ∈ V
102		difexg 5246	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V)
103	9	elrnmpt 5854	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)))
104	101, 102, 103	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
105	100, 104	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
106	105	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
107	89, 96, 106	rspcdva 3554	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅)
108		ssdif0 4294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅)
109	107, 108	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶)
110	109	ralrimiva 3107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
111		unissb 4870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝐴 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
112	110, 111	sylibr 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶)
113		elssuni 4868	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴)
114	113	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴)
115	112, 114	eqssd 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶)
116		simpll 763	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴)
117	115, 116	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴)
118	117	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
119	87, 88, 118	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
120	86, 119	mtod 197	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶)
121	28	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴)
122		simplrl 773	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴)
123		sorpssi 7560	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
124	121, 122, 87, 123	syl12anc 833	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
125		orel1 885	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓))
126	120, 124, 125	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓)
127		undif 4412	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
128	126, 127	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
129	85, 128	sseq12d 3950	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓))
130		ssun1 4102	. . . . . . . . . . . . 13 ⊢ ℎ ⊆ (ℎ ∪ 𝐶)
131		sstr 3925	. . . . . . . . . . . . 13 ⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓)
132	130, 131	mpan 686	. . . . . . . . . . . 12 ⊢ ((ℎ ∪ 𝐶) ⊆ 𝑓 → ℎ ⊆ 𝑓)
133	129, 132	syl6bi 252	. . . . . . . . . . 11 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) → ℎ ⊆ 𝑓))
134	81, 133	syl5 34	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → ℎ ⊆ 𝑓))
135	80, 134	mpd 15	. . . . . . . . 9 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ℎ ⊆ 𝑓)
136	135	ralrimiva 3107	. . . . . . . 8 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
137		unissb 4870	. . . . . . . 8 ⊢ (∪ 𝐴 ⊆ 𝑓 ↔ ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
138	136, 137	sylibr 233	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ⊆ 𝑓)
139		elssuni 4868	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴)
140	139	ad2antrl 724	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴)
141	138, 140	eqssd 3934	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 = 𝑓)
142		simprl 767	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴)
143	141, 142	eqeltrd 2839	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ∈ 𝐴)
144	143	rexlimdvaa 3213	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶) → ∪ 𝐴 ∈ 𝐴))
145	65, 144	syl5 34	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∪ 𝐴 ∈ 𝐴))
146	61, 145	mtod 197	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ¬ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
147	60, 146	pm2.65da 813	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ Fin^II)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ⊆ wss 3883 ∅c0 4253 𝒫 cpw 4530 ∪ cuni 4836 ↦ cmpt 5153 Or wor 5493 ran crn 5581 [⊊] crpss 7553 Fincfn 8691 Fin^IIcfin2 9966

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-po 5494 df-so 5495 df-xp 5586 df-rel 5587 df-cnv 5588 df-dm 5590 df-rn 5591 df-rpss 7554 df-fin2 9973

This theorem is referenced by: fin1a2s 10101

W3C validator