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 10177

Description: Lemma for fin1a2 10180. (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 485	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → (𝐵 ∖ 𝐶) ∈ Fin^II)
2		simpll1 1211	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐴 ⊆ 𝒫 𝐵)
3		ssel2 3917	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ∈ 𝒫 𝐵)
4	3	elpwid 4545	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → 𝑔 ⊆ 𝐵)
5	4	ssdifd 4076	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
6		sseq1 3947	. . . . . . . 8 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝐵 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶)))
7	5, 6	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴) → (𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
8	7	rexlimdva 3214	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → 𝑓 ⊆ (𝐵 ∖ 𝐶)))
9		eqid 2739	. . . . . . . 8 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))
10	9	elrnmpt 5868	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶)))
11	10	elv 3439	. . . . . 6 ⊢ (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶))
12		velpw 4539	. . . . . 6 ⊢ (𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶) ↔ 𝑓 ⊆ (𝐵 ∖ 𝐶))
13	8, 11, 12	3imtr4g 296	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐵 → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → 𝑓 ∈ 𝒫 (𝐵 ∖ 𝐶)))
14	13	ssrdv 3928	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
15	2, 14	syl 17	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶))
16		simplrr 775	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → 𝐶 ∈ 𝐴)
17		difid 4305	. . . . . . 7 ⊢ (𝐶 ∖ 𝐶) = ∅
18	17	eqcomi 2748	. . . . . 6 ⊢ ∅ = (𝐶 ∖ 𝐶)
19		difeq1 4051	. . . . . . 7 ⊢ (𝑔 = 𝐶 → (𝑔 ∖ 𝐶) = (𝐶 ∖ 𝐶))
20	19	rspceeqv 3576	. . . . . 6 ⊢ ((𝐶 ∈ 𝐴 ∧ ∅ = (𝐶 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
21	18, 20	mpan2 688	. . . . 5 ⊢ (𝐶 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
22		0ex 5232	. . . . . 6 ⊢ ∅ ∈ V
23	9	elrnmpt 5868	. . . . . 6 ⊢ (∅ ∈ V → (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶)))
24	22, 23	ax-mp 5	. . . . 5 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 ∅ = (𝑔 ∖ 𝐶))
25	21, 24	sylibr 233	. . . 4 ⊢ (𝐶 ∈ 𝐴 → ∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
26		ne0i 4269	. . . 4 ⊢ (∅ ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
27	16, 25, 26	3syl 18	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅)
28		simpll2 1212	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → [⊊] Or 𝐴)
29	9	elrnmpt 5868	. . . . . . . 8 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶)))
30	29	elv 3439	. . . . . . 7 ⊢ (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶))
31		difeq1 4051	. . . . . . . . . 10 ⊢ (𝑔 = 𝑒 → (𝑔 ∖ 𝐶) = (𝑒 ∖ 𝐶))
32	31	eqeq2d 2750	. . . . . . . . 9 ⊢ (𝑔 = 𝑒 → (𝑥 = (𝑔 ∖ 𝐶) ↔ 𝑥 = (𝑒 ∖ 𝐶)))
33	32	cbvrexvw 3385	. . . . . . . 8 ⊢ (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) ↔ ∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶))
34		sorpssi 7591	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒))
35		ssdif 4075	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ⊆ 𝑔 → (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶))
36		ssdif 4075	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ⊆ 𝑒 → (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))
37	35, 36	orim12i 906	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
38	34, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
39		sseq2 3948	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶)))
40		sseq1 3947	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (𝑓 ⊆ (𝑒 ∖ 𝐶) ↔ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶)))
41	39, 40	orbi12d 916	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝑔 ∖ 𝐶) → (((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)) ↔ ((𝑒 ∖ 𝐶) ⊆ (𝑔 ∖ 𝐶) ∨ (𝑔 ∖ 𝐶) ⊆ (𝑒 ∖ 𝐶))))
42	38, 41	syl5ibrcom 246	. . . . . . . . . . . . . 14 ⊢ (( [⊊] Or 𝐴 ∧ (𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
43	42	expr 457	. . . . . . . . . . . . 13 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑔 ∈ 𝐴 → (𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))))
44	43	rexlimdv 3213	. . . . . . . . . . . 12 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (∃𝑔 ∈ 𝐴 𝑓 = (𝑔 ∖ 𝐶) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
45	11, 44	syl5bi 241	. . . . . . . . . . 11 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
46	45	ralrimiv 3103	. . . . . . . . . 10 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
47		sseq1 3947	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑥 ⊆ 𝑓 ↔ (𝑒 ∖ 𝐶) ⊆ 𝑓))
48		sseq2 3948	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑒 ∖ 𝐶)))
49	47, 48	orbi12d 916	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → ((𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
50	49	ralbidv 3113	. . . . . . . . . 10 ⊢ (𝑥 = (𝑒 ∖ 𝐶) → (∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥) ↔ ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))((𝑒 ∖ 𝐶) ⊆ 𝑓 ∨ 𝑓 ⊆ (𝑒 ∖ 𝐶))))
51	46, 50	syl5ibrcom 246	. . . . . . . . 9 ⊢ (( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴) → (𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
52	51	rexlimdva 3214	. . . . . . . 8 ⊢ ( [⊊] Or 𝐴 → (∃𝑒 ∈ 𝐴 𝑥 = (𝑒 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
53	33, 52	syl5bi 241	. . . . . . 7 ⊢ ( [⊊] Or 𝐴 → (∃𝑔 ∈ 𝐴 𝑥 = (𝑔 ∖ 𝐶) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
54	30, 53	syl5bi 241	. . . . . 6 ⊢ ( [⊊] Or 𝐴 → (𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥)))
55	54	ralrimiv 3103	. . . . 5 ⊢ ( [⊊] Or 𝐴 → ∀𝑥 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))∀𝑓 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))(𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥))
56		sorpss 7590	. . . . 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 10060	. . 3 ⊢ ((((𝐵 ∖ 𝐶) ∈ Fin^II ∧ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ⊆ 𝒫 (𝐵 ∖ 𝐶)) ∧ (ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ≠ ∅ ∧ [⊊] Or ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
60	1, 15, 27, 58, 59	syl22anc 836	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
61		simpll3 1213	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) → ¬ ∪ 𝐴 ∈ 𝐴)
62		difeq1 4051	. . . . . . 7 ⊢ (𝑔 = 𝑓 → (𝑔 ∖ 𝐶) = (𝑓 ∖ 𝐶))
63	62	cbvmptv 5188	. . . . . 6 ⊢ (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∈ 𝐴 ↦ (𝑓 ∖ 𝐶))
64	63	elrnmpt 5868	. . . . 5 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)))
65	64	ibi 266	. . . 4 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → ∃𝑓 ∈ 𝐴 ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
66		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)
67		difeq1 4051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = ℎ → (𝑔 ∖ 𝐶) = (ℎ ∖ 𝐶))
68	67	rspceeqv 3576	. . . . . . . . . . . . . . . 16 ⊢ ((ℎ ∈ 𝐴 ∧ (ℎ ∖ 𝐶) = (ℎ ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
69	66, 68	mpan2 688	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
70	69	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
71		vex 3437	. . . . . . . . . . . . . . 15 ⊢ ℎ ∈ V
72		difexg 5252	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ V → (ℎ ∖ 𝐶) ∈ V)
73	9	elrnmpt 5868	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∈ V → ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶)))
74	71, 72, 73	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (ℎ ∖ 𝐶) = (𝑔 ∖ 𝐶))
75	70, 74	sylibr 233	. . . . . . . . . . . . 13 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
76		elssuni 4872	. . . . . . . . . . . . 13 ⊢ ((ℎ ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
77	75, 76	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
78		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
79	77, 78	sseqtrd 3962	. . . . . . . . . . 11 ⊢ (((𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
80	79	adantll 711	. . . . . . . . . 10 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶))
81		unss2 4116	. . . . . . . . . . 11 ⊢ ((ℎ ∖ 𝐶) ⊆ (𝑓 ∖ 𝐶) → (𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)))
82		uncom 4088	. . . . . . . . . . . . . . 15 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = ((ℎ ∖ 𝐶) ∪ 𝐶)
83		undif1 4410	. . . . . . . . . . . . . . 15 ⊢ ((ℎ ∖ 𝐶) ∪ 𝐶) = (ℎ ∪ 𝐶)
84	82, 83	eqtri 2767	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶)
85	84	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (ℎ ∖ 𝐶)) = (ℎ ∪ 𝐶))
86	61	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ ∪ 𝐴 ∈ 𝐴)
87	16	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ∈ 𝐴)
88		simplrr 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
89		eqeq1 2743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑒 = (𝑥 ∖ 𝐶) → (𝑒 = ∅ ↔ (𝑥 ∖ 𝐶) = ∅))
90		simpllr 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))
91		ssdif0 4298	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ⊆ 𝐶 ↔ (𝑓 ∖ 𝐶) = ∅)
92	91	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 ⊆ 𝐶 → (𝑓 ∖ 𝐶) = ∅)
93	92	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑓 ∖ 𝐶) = ∅)
94	90, 93	eqtrd 2779	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅)
95		uni0c 4869	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = ∅ ↔ ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
96	94, 95	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → ∀𝑒 ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶))𝑒 = ∅)
97		eqid 2739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)
98		difeq1 4051	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑔 = 𝑥 → (𝑔 ∖ 𝐶) = (𝑥 ∖ 𝐶))
99	98	rspceeqv 3576	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝑥 ∖ 𝐶) = (𝑥 ∖ 𝐶)) → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
100	97, 99	mpan2 688	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 ∈ 𝐴 → ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
101		vex 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑥 ∈ V
102		difexg 5252	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 ∈ V → (𝑥 ∖ 𝐶) ∈ V)
103	9	elrnmpt 5868	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑥 ∖ 𝐶) ∈ V → ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶)))
104	101, 102, 103	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) ↔ ∃𝑔 ∈ 𝐴 (𝑥 ∖ 𝐶) = (𝑔 ∖ 𝐶))
105	100, 104	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐴 → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
106	105	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) ∈ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)))
107	89, 96, 106	rspcdva 3563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∖ 𝐶) = ∅)
108		ssdif0 4298	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ⊆ 𝐶 ↔ (𝑥 ∖ 𝐶) = ∅)
109	107, 108	sylibr 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) ∧ 𝑥 ∈ 𝐴) → 𝑥 ⊆ 𝐶)
110	109	ralrimiva 3104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
111		unissb 4874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∪ 𝐴 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶)
112	110, 111	sylibr 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ⊆ 𝐶)
113		elssuni 4872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴)
114	113	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ⊆ ∪ 𝐴)
115	112, 114	eqssd 3939	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 = 𝐶)
116		simpll 764	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → 𝐶 ∈ 𝐴)
117	115, 116	eqeltrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) ∧ 𝑓 ⊆ 𝐶) → ∪ 𝐴 ∈ 𝐴)
118	117	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶)) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
119	87, 88, 118	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴))
120	86, 119	mtod 197	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ¬ 𝑓 ⊆ 𝐶)
121	28	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → [⊊] Or 𝐴)
122		simplrl 774	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝑓 ∈ 𝐴)
123		sorpssi 7591	. . . . . . . . . . . . . . . 16 ⊢ (( [⊊] Or 𝐴 ∧ (𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
124	121, 122, 87, 123	syl12anc 834	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓))
125		orel1 886	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑓 ⊆ 𝐶 → ((𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓) → 𝐶 ⊆ 𝑓))
126	120, 124, 125	sylc 65	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → 𝐶 ⊆ 𝑓)
127		undif 4416	. . . . . . . . . . . . . 14 ⊢ (𝐶 ⊆ 𝑓 ↔ (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
128	126, 127	sylib 217	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → (𝐶 ∪ (𝑓 ∖ 𝐶)) = 𝑓)
129	85, 128	sseq12d 3955	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) ∧ ℎ ∈ 𝐴) → ((𝐶 ∪ (ℎ ∖ 𝐶)) ⊆ (𝐶 ∪ (𝑓 ∖ 𝐶)) ↔ (ℎ ∪ 𝐶) ⊆ 𝑓))
130		ssun1 4107	. . . . . . . . . . . . 13 ⊢ ℎ ⊆ (ℎ ∪ 𝐶)
131		sstr 3930	. . . . . . . . . . . . 13 ⊢ ((ℎ ⊆ (ℎ ∪ 𝐶) ∧ (ℎ ∪ 𝐶) ⊆ 𝑓) → ℎ ⊆ 𝑓)
132	130, 131	mpan 687	. . . . . . . . . . . 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 3104	. . . . . . . 8 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
137		unissb 4874	. . . . . . . 8 ⊢ (∪ 𝐴 ⊆ 𝑓 ↔ ∀ℎ ∈ 𝐴 ℎ ⊆ 𝑓)
138	136, 137	sylibr 233	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ⊆ 𝑓)
139		elssuni 4872	. . . . . . . 8 ⊢ (𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴)
140	139	ad2antrl 725	. . . . . . 7 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ⊆ ∪ 𝐴)
141	138, 140	eqssd 3939	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 = 𝑓)
142		simprl 768	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → 𝑓 ∈ 𝐴)
143	141, 142	eqeltrd 2840	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) ∧ (𝐵 ∖ 𝐶) ∈ Fin^II) ∧ (𝑓 ∈ 𝐴 ∧ ∪ ran (𝑔 ∈ 𝐴 ↦ (𝑔 ∖ 𝐶)) = (𝑓 ∖ 𝐶))) → ∪ 𝐴 ∈ 𝐴)
144	143	rexlimdvaa 3215	. . . 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 814	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∖ 𝐶) ∈ Fin^II)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2944 ∀wral 3065 ∃wrex 3066 Vcvv 3433 ∖ cdif 3885 ∪ cun 3886 ⊆ wss 3888 ∅c0 4257 𝒫 cpw 4534 ∪ cuni 4840 ↦ cmpt 5158 Or wor 5503 ran crn 5591 [⊊] crpss 7584 Fincfn 8742 Fin^IIcfin2 10044

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-br 5076 df-opab 5138 df-mpt 5159 df-po 5504 df-so 5505 df-xp 5596 df-rel 5597 df-cnv 5598 df-dm 5600 df-rn 5601 df-rpss 7585 df-fin2 10051

This theorem is referenced by: fin1a2s 10179

W3C validator