Metamath Proof Explorer

Theorem fin1a2lem13

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

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ( 𝐵 ∖ 𝐶 ) ∈ FinII )
2 simpll1 ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → 𝐴 ⊆ 𝒫 𝐵 )
3 ssel2 ⊢ ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ 𝒫 𝐵 )
4 3 elpwid ⊢ ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ⊆ 𝐵 )
5 4 ssdifd ⊢ ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝐵 ∖ 𝐶 ) )
6 sseq1 ⊢ ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( 𝑓 ⊆ ( 𝐵 ∖ 𝐶 ) ↔ ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝐵 ∖ 𝐶 ) ) )
7 5 6 syl5ibrcom ⊢ ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → 𝑓 ⊆ ( 𝐵 ∖ 𝐶 ) ) )
8 7 rexlimdva ⊢ ( 𝐴 ⊆ 𝒫 𝐵 → ( ∃ 𝑔 ∈ 𝐴 𝑓 = ( 𝑔 ∖ 𝐶 ) → 𝑓 ⊆ ( 𝐵 ∖ 𝐶 ) ) )
9 eqid ⊢ ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) )
10 9 elrnmpt ⊢ ( 𝑓 ∈ V → ( 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 𝑓 = ( 𝑔 ∖ 𝐶 ) ) )
11 10 elv ⊢ ( 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 𝑓 = ( 𝑔 ∖ 𝐶 ) )
12 velpw ⊢ ( 𝑓 ∈ 𝒫 ( 𝐵 ∖ 𝐶 ) ↔ 𝑓 ⊆ ( 𝐵 ∖ 𝐶 ) )
13 8 11 12 3imtr4g ⊢ ( 𝐴 ⊆ 𝒫 𝐵 → ( 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → 𝑓 ∈ 𝒫 ( 𝐵 ∖ 𝐶 ) ) )
14 13 ssrdv ⊢ ( 𝐴 ⊆ 𝒫 𝐵 → ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ⊆ 𝒫 ( 𝐵 ∖ 𝐶 ) )
15 2 14 syl ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ⊆ 𝒫 ( 𝐵 ∖ 𝐶 ) )
16 simplrr ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → 𝐶 ∈ 𝐴 )
17 difid ⊢ ( 𝐶 ∖ 𝐶 ) = ∅
18 17 eqcomi ⊢ ∅ = ( 𝐶 ∖ 𝐶 )
19 difeq1 ⊢ ( 𝑔 = 𝐶 → ( 𝑔 ∖ 𝐶 ) = ( 𝐶 ∖ 𝐶 ) )
20 19 rspceeqv ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∅ = ( 𝐶 ∖ 𝐶 ) ) → ∃ 𝑔 ∈ 𝐴 ∅ = ( 𝑔 ∖ 𝐶 ) )
21 18 20 mpan2 ⊢ ( 𝐶 ∈ 𝐴 → ∃ 𝑔 ∈ 𝐴 ∅ = ( 𝑔 ∖ 𝐶 ) )
22 0ex ⊢ ∅ ∈ V
23 9 elrnmpt ⊢ ( ∅ ∈ V → ( ∅ ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ∅ = ( 𝑔 ∖ 𝐶 ) ) )
24 22 23 ax-mp ⊢ ( ∅ ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ∅ = ( 𝑔 ∖ 𝐶 ) )
25 21 24 sylibr ⊢ ( 𝐶 ∈ 𝐴 → ∅ ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
26 ne0i ⊢ ( ∅ ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ≠ ∅ )
27 16 25 26 3syl ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ≠ ∅ )
28 simpll2 ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → [⊊] Or 𝐴 )
29 9 elrnmpt ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 𝑥 = ( 𝑔 ∖ 𝐶 ) ) )
30 29 elv ⊢ ( 𝑥 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 𝑥 = ( 𝑔 ∖ 𝐶 ) )
31 difeq1 ⊢ ( 𝑔 = 𝑒 → ( 𝑔 ∖ 𝐶 ) = ( 𝑒 ∖ 𝐶 ) )
32 31 eqeq2d ⊢ ( 𝑔 = 𝑒 → ( 𝑥 = ( 𝑔 ∖ 𝐶 ) ↔ 𝑥 = ( 𝑒 ∖ 𝐶 ) ) )
33 32 cbvrexvw ⊢ ( ∃ 𝑔 ∈ 𝐴 𝑥 = ( 𝑔 ∖ 𝐶 ) ↔ ∃ 𝑒 ∈ 𝐴 𝑥 = ( 𝑒 ∖ 𝐶 ) )
34 sorpssi ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) → ( 𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒 ) )
35 ssdif ⊢ ( 𝑒 ⊆ 𝑔 → ( 𝑒 ∖ 𝐶 ) ⊆ ( 𝑔 ∖ 𝐶 ) )
36 ssdif ⊢ ( 𝑔 ⊆ 𝑒 → ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝑒 ∖ 𝐶 ) )
37 35 36 orim12i ⊢ ( ( 𝑒 ⊆ 𝑔 ∨ 𝑔 ⊆ 𝑒 ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ ( 𝑔 ∖ 𝐶 ) ∨ ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝑒 ∖ 𝐶 ) ) )
38 34 37 syl ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ ( 𝑔 ∖ 𝐶 ) ∨ ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝑒 ∖ 𝐶 ) ) )
39 sseq2 ⊢ ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ↔ ( 𝑒 ∖ 𝐶 ) ⊆ ( 𝑔 ∖ 𝐶 ) ) )
40 sseq1 ⊢ ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ↔ ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝑒 ∖ 𝐶 ) ) )
41 39 40 orbi12d ⊢ ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ↔ ( ( 𝑒 ∖ 𝐶 ) ⊆ ( 𝑔 ∖ 𝐶 ) ∨ ( 𝑔 ∖ 𝐶 ) ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
42 38 41 syl5ibrcom ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) → ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
43 42 expr ⊢ ( ( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴 ) → ( 𝑔 ∈ 𝐴 → ( 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) ) )
44 43 rexlimdv ⊢ ( ( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴 ) → ( ∃ 𝑔 ∈ 𝐴 𝑓 = ( 𝑔 ∖ 𝐶 ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
45 11 44 biimtrid ⊢ ( ( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴 ) → ( 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
46 45 ralrimiv ⊢ ( ( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴 ) → ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) )
47 sseq1 ⊢ ( 𝑥 = ( 𝑒 ∖ 𝐶 ) → ( 𝑥 ⊆ 𝑓 ↔ ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ) )
48 sseq2 ⊢ ( 𝑥 = ( 𝑒 ∖ 𝐶 ) → ( 𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) )
49 47 48 orbi12d ⊢ ( 𝑥 = ( 𝑒 ∖ 𝐶 ) → ( ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ↔ ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
50 49 ralbidv ⊢ ( 𝑥 = ( 𝑒 ∖ 𝐶 ) → ( ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ↔ ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( ( 𝑒 ∖ 𝐶 ) ⊆ 𝑓 ∨ 𝑓 ⊆ ( 𝑒 ∖ 𝐶 ) ) ) )
51 46 50 syl5ibrcom ⊢ ( ( [⊊] Or 𝐴 ∧ 𝑒 ∈ 𝐴 ) → ( 𝑥 = ( 𝑒 ∖ 𝐶 ) → ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ) )
52 51 rexlimdva ⊢ ( [⊊] Or 𝐴 → ( ∃ 𝑒 ∈ 𝐴 𝑥 = ( 𝑒 ∖ 𝐶 ) → ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ) )
53 33 52 biimtrid ⊢ ( [⊊] Or 𝐴 → ( ∃ 𝑔 ∈ 𝐴 𝑥 = ( 𝑔 ∖ 𝐶 ) → ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ) )
54 30 53 biimtrid ⊢ ( [⊊] Or 𝐴 → ( 𝑥 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) ) )
55 54 ralrimiv ⊢ ( [⊊] Or 𝐴 → ∀ 𝑥 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) )
56 sorpss ⊢ ( [⊊] Or ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∀ 𝑓 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ( 𝑥 ⊆ 𝑓 ∨ 𝑓 ⊆ 𝑥 ) )
57 55 56 sylibr ⊢ ( [⊊] Or 𝐴 → [⊊] Or ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
58 28 57 syl ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → [⊊] Or ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
59 fin2i ⊢ ( ( ( ( 𝐵 ∖ 𝐶 ) ∈ FinII ∧ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ⊆ 𝒫 ( 𝐵 ∖ 𝐶 ) ) ∧ ( ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ≠ ∅ ∧ [⊊] Or ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ) ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
60 1 15 27 58 59 syl22anc ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
61 simpll3 ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ¬ ∪ 𝐴 ∈ 𝐴 )
62 difeq1 ⊢ ( 𝑔 = 𝑓 → ( 𝑔 ∖ 𝐶 ) = ( 𝑓 ∖ 𝐶 ) )
63 62 cbvmptv ⊢ ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∈ 𝐴 ↦ ( 𝑓 ∖ 𝐶 ) )
64 63 elrnmpt ⊢ ( ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ( ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑓 ∈ 𝐴 ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) )
65 64 ibi ⊢ ( ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ∃ 𝑓 ∈ 𝐴 ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) )
66 eqid ⊢ ( ℎ ∖ 𝐶 ) = ( ℎ ∖ 𝐶 )
67 difeq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ∖ 𝐶 ) = ( ℎ ∖ 𝐶 ) )
68 67 rspceeqv ⊢ ( ( ℎ ∈ 𝐴 ∧ ( ℎ ∖ 𝐶 ) = ( ℎ ∖ 𝐶 ) ) → ∃ 𝑔 ∈ 𝐴 ( ℎ ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
69 66 68 mpan2 ⊢ ( ℎ ∈ 𝐴 → ∃ 𝑔 ∈ 𝐴 ( ℎ ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
70 69 adantl ⊢ ( ( ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ ℎ ∈ 𝐴 ) → ∃ 𝑔 ∈ 𝐴 ( ℎ ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
71 vex ⊢ ℎ ∈ V
72 difexg ⊢ ( ℎ ∈ V → ( ℎ ∖ 𝐶 ) ∈ V )
73 9 elrnmpt ⊢ ( ( ℎ ∖ 𝐶 ) ∈ V → ( ( ℎ ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ( ℎ ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) ) )
74 71 72 73 mp2b ⊢ ( ( ℎ ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ( ℎ ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
75 70 74 sylibr ⊢ ( ( ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ ℎ ∈ 𝐴 ) → ( ℎ ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
76 elssuni ⊢ ( ( ℎ ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ( ℎ ∖ 𝐶 ) ⊆ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
77 75 76 syl ⊢ ( ( ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ ℎ ∈ 𝐴 ) → ( ℎ ∖ 𝐶 ) ⊆ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
78 simplr ⊢ ( ( ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ ℎ ∈ 𝐴 ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) )
79 77 78 sseqtrd ⊢ ( ( ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ ℎ ∈ 𝐴 ) → ( ℎ ∖ 𝐶 ) ⊆ ( 𝑓 ∖ 𝐶 ) )
80 79 adantll ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( ℎ ∖ 𝐶 ) ⊆ ( 𝑓 ∖ 𝐶 ) )
81 unss2 ⊢ ( ( ℎ ∖ 𝐶 ) ⊆ ( 𝑓 ∖ 𝐶 ) → ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) ⊆ ( 𝐶 ∪ ( 𝑓 ∖ 𝐶 ) ) )
82 uncom ⊢ ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) = ( ( ℎ ∖ 𝐶 ) ∪ 𝐶 )
83 undif1 ⊢ ( ( ℎ ∖ 𝐶 ) ∪ 𝐶 ) = ( ℎ ∪ 𝐶 )
84 82 83 eqtri ⊢ ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) = ( ℎ ∪ 𝐶 )
85 84 a1i ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) = ( ℎ ∪ 𝐶 ) )
86 61 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ¬ ∪ 𝐴 ∈ 𝐴 )
87 16 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → 𝐶 ∈ 𝐴 )
88 simplrr ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) )
89 eqeq1 ⊢ ( 𝑒 = ( 𝑥 ∖ 𝐶 ) → ( 𝑒 = ∅ ↔ ( 𝑥 ∖ 𝐶 ) = ∅ ) )
90 simpllr ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) )
91 ssdif0 ⊢ ( 𝑓 ⊆ 𝐶 ↔ ( 𝑓 ∖ 𝐶 ) = ∅ )
92 91 biimpi ⊢ ( 𝑓 ⊆ 𝐶 → ( 𝑓 ∖ 𝐶 ) = ∅ )
93 92 ad2antlr ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑓 ∖ 𝐶 ) = ∅ )
94 90 93 eqtrd ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ∅ )
95 uni0c ⊢ ( ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ∅ ↔ ∀ 𝑒 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) 𝑒 = ∅ )
96 94 95 sylib ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑒 ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) 𝑒 = ∅ )
97 eqid ⊢ ( 𝑥 ∖ 𝐶 ) = ( 𝑥 ∖ 𝐶 )
98 difeq1 ⊢ ( 𝑔 = 𝑥 → ( 𝑔 ∖ 𝐶 ) = ( 𝑥 ∖ 𝐶 ) )
99 98 rspceeqv ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∖ 𝐶 ) = ( 𝑥 ∖ 𝐶 ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑥 ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
100 97 99 mpan2 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑔 ∈ 𝐴 ( 𝑥 ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
101 vex ⊢ 𝑥 ∈ V
102 difexg ⊢ ( 𝑥 ∈ V → ( 𝑥 ∖ 𝐶 ) ∈ V )
103 9 elrnmpt ⊢ ( ( 𝑥 ∖ 𝐶 ) ∈ V → ( ( 𝑥 ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑥 ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) ) )
104 101 102 103 mp2b ⊢ ( ( 𝑥 ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ↔ ∃ 𝑔 ∈ 𝐴 ( 𝑥 ∖ 𝐶 ) = ( 𝑔 ∖ 𝐶 ) )
105 100 104 sylibr ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
106 105 adantl ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∖ 𝐶 ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
107 89 96 106 rspcdva ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∖ 𝐶 ) = ∅ )
108 ssdif0 ⊢ ( 𝑥 ⊆ 𝐶 ↔ ( 𝑥 ∖ 𝐶 ) = ∅ )
109 107 108 sylibr ⊢ ( ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ⊆ 𝐶 )
110 109 ralrimiva ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶 )
111 unissb ⊢ ( ∪ 𝐴 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐶 )
112 110 111 sylibr ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → ∪ 𝐴 ⊆ 𝐶 )
113 elssuni ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ⊆ ∪ 𝐴 )
114 113 ad2antrr ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → 𝐶 ⊆ ∪ 𝐴 )
115 112 114 eqssd ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → ∪ 𝐴 = 𝐶 )
116 simpll ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → 𝐶 ∈ 𝐴 )
117 115 116 eqeltrd ⊢ ( ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ∧ 𝑓 ⊆ 𝐶 ) → ∪ 𝐴 ∈ 𝐴 )
118 117 ex ⊢ ( ( 𝐶 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) → ( 𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴 ) )
119 87 88 118 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( 𝑓 ⊆ 𝐶 → ∪ 𝐴 ∈ 𝐴 ) )
120 86 119 mtod ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ¬ 𝑓 ⊆ 𝐶 )
121 28 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → [⊊] Or 𝐴 )
122 simplrl ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → 𝑓 ∈ 𝐴 )
123 sorpssi ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝑓 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓 ) )
124 121 122 87 123 syl12anc ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( 𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓 ) )
125 orel1 ⊢ ( ¬ 𝑓 ⊆ 𝐶 → ( ( 𝑓 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝑓 ) → 𝐶 ⊆ 𝑓 ) )
126 120 124 125 sylc ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → 𝐶 ⊆ 𝑓 )
127 undif ⊢ ( 𝐶 ⊆ 𝑓 ↔ ( 𝐶 ∪ ( 𝑓 ∖ 𝐶 ) ) = 𝑓 )
128 126 127 sylib ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( 𝐶 ∪ ( 𝑓 ∖ 𝐶 ) ) = 𝑓 )
129 85 128 sseq12d ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) ⊆ ( 𝐶 ∪ ( 𝑓 ∖ 𝐶 ) ) ↔ ( ℎ ∪ 𝐶 ) ⊆ 𝑓 ) )
130 ssun1 ⊢ ℎ ⊆ ( ℎ ∪ 𝐶 )
131 sstr ⊢ ( ( ℎ ⊆ ( ℎ ∪ 𝐶 ) ∧ ( ℎ ∪ 𝐶 ) ⊆ 𝑓 ) → ℎ ⊆ 𝑓 )
132 130 131 mpan ⊢ ( ( ℎ ∪ 𝐶 ) ⊆ 𝑓 → ℎ ⊆ 𝑓 )
133 129 132 biimtrdi ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( ( 𝐶 ∪ ( ℎ ∖ 𝐶 ) ) ⊆ ( 𝐶 ∪ ( 𝑓 ∖ 𝐶 ) ) → ℎ ⊆ 𝑓 ) )
134 81 133 syl5 ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ( ( ℎ ∖ 𝐶 ) ⊆ ( 𝑓 ∖ 𝐶 ) → ℎ ⊆ 𝑓 ) )
135 80 134 mpd ⊢ ( ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) ∧ ℎ ∈ 𝐴 ) → ℎ ⊆ 𝑓 )
136 135 ralrimiva ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → ∀ ℎ ∈ 𝐴 ℎ ⊆ 𝑓 )
137 unissb ⊢ ( ∪ 𝐴 ⊆ 𝑓 ↔ ∀ ℎ ∈ 𝐴 ℎ ⊆ 𝑓 )
138 136 137 sylibr ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → ∪ 𝐴 ⊆ 𝑓 )
139 elssuni ⊢ ( 𝑓 ∈ 𝐴 → 𝑓 ⊆ ∪ 𝐴 )
140 139 ad2antrl ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → 𝑓 ⊆ ∪ 𝐴 )
141 138 140 eqssd ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → ∪ 𝐴 = 𝑓 )
142 simprl ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → 𝑓 ∈ 𝐴 )
143 141 142 eqeltrd ⊢ ( ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) ∧ ( 𝑓 ∈ 𝐴 ∧ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) ) ) → ∪ 𝐴 ∈ 𝐴 )
144 143 rexlimdvaa ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ( ∃ 𝑓 ∈ 𝐴 ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) = ( 𝑓 ∖ 𝐶 ) → ∪ 𝐴 ∈ 𝐴 ) )
145 65 144 syl5 ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ( ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) → ∪ 𝐴 ∈ 𝐴 ) )
146 61 145 mtod ⊢ ( ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) ∧ ( 𝐵 ∖ 𝐶 ) ∈ FinII ) → ¬ ∪ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) ∈ ran ( 𝑔 ∈ 𝐴 ↦ ( 𝑔 ∖ 𝐶 ) ) )
147 60 146 pm2.65da ⊢ ( ( ( 𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴 ) ∧ ( ¬ 𝐶 ∈ Fin ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 ∖ 𝐶 ) ∈ FinII )