fin1a2lem12 - Metamath Proof Explorer

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

Theorem fin1a2lem12 10413

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

**Assertion**
Ref	Expression
fin1a2lem12	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Proof of Theorem fin1a2lem12 Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐵 ∈ Fin^III)
2		simpll1 1231	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ⊆ 𝒫 𝐵)
3	2	adantr 486	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4		ssrab2 4037	. . . . . . . 8 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐴
5	4	unissi 4886	. . . . . . 7 ⊢ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ ∪ 𝐴
6		sspwuni 5071	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
7	6	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ 𝐴 ⊆ 𝐵)
8	5, 7	sstrid 3951	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
9	3, 8	syl 18	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
10		elpw2g 5309	. . . . . 6 ⊢ (𝐵 ∈ Fin^III → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
11	10	ad2antlr 740	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
12	9, 11	mpbird 260	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵)
13	12	fmpttd 7117	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵)
14		vex 3462	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
15	14	sucex 7814	. . . . . . . . . 10 ⊢ suc 𝑑 ∈ V
16		sssucid 6450	. . . . . . . . . 10 ⊢ 𝑑 ⊆ suc 𝑑
17		ssdomg 9006	. . . . . . . . . 10 ⊢ (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑 → 𝑑 ≼ suc 𝑑))
18	15, 16, 17	mp2 9	. . . . . . . . 9 ⊢ 𝑑 ≼ suc 𝑑
19		domtr 9013	. . . . . . . . 9 ⊢ ((𝑓 ≼ 𝑑 ∧ 𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
20	18, 19	mpan2 704	. . . . . . . 8 ⊢ (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐴 → (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑))
22	21	ss2rabi 4033	. . . . . 6 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑}
23		uniss 4885	. . . . . 6 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
24	22, 23	mp1i 14	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
25		id 23	. . . . . 6 ⊢ (𝑑 ∈ ω → 𝑑 ∈ ω)
26		pwexg 5354	. . . . . . . . 9 ⊢ (𝐵 ∈ Fin^III → 𝒫 𝐵 ∈ V)
27	26	adantl 487	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝒫 𝐵 ∈ V)
28	27, 2	ssexd 5300	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ∈ V)
29		rabexg 5313	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
30		uniexg 7751	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
31	28, 29, 30	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
32		breq2 5118	. . . . . . . . 9 ⊢ (𝑒 = 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ 𝑑))
33	32	rabbidv 3426	. . . . . . . 8 ⊢ (𝑒 = 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
34	33	unieqd 4890	. . . . . . 7 ⊢ (𝑒 = 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
35		eqid 2766	. . . . . . 7 ⊢ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})
36	34, 35	fvmptg 6994	. . . . . 6 ⊢ ((𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
37	25, 31, 36	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
38		peano2 7895	. . . . . 6 ⊢ (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39		rabexg 5313	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
40		uniexg 7751	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
41	28, 39, 40	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
42		breq2 5118	. . . . . . . . 9 ⊢ (𝑒 = suc 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ suc 𝑑))
43	42	rabbidv 3426	. . . . . . . 8 ⊢ (𝑒 = suc 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
44	43	unieqd 4890	. . . . . . 7 ⊢ (𝑒 = suc 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
45	44, 35	fvmptg 6994	. . . . . 6 ⊢ ((suc 𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
46	38, 41, 45	syl2anr 609	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
47	24, 37, 46	3sstr4d 3995	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
48	47	ralrimiva 3160	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
49		fin34i 10383	. . 3 ⊢ ((𝐵 ∈ Fin^III ∧ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑)) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
50	1, 13, 48, 49	syl3anc 1398	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
51		fin1a2lem11 10412	. . . . . 6 ⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
52	51	adantrr 730	. . . . 5 ⊢ (( [⊊] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
53	52	3ad2antl2 1205	. . . 4 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
54	53	adantr 486	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
55		simpll3 1233	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 ∈ 𝐴)
56		simplrr 790	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ≠ ∅)
57		sspwuni 5071	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 ⊆ ∅)
58		ss0b 4361	. . . . . . . . . . 11 ⊢ (∪ 𝐴 ⊆ ∅ ↔ ∪ 𝐴 = ∅)
59	57, 58	bitri 278	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 = ∅)
60		pw0 4783	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
61	60	sseq2i 3969	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62		sssn 4797	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
63	61, 62	bitri 278	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64		df-ne 2962	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65		0ex 5275	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
66	65	unisn 4896	. . . . . . . . . . . . . . . 16 ⊢ ∪ {∅} = ∅
67	65	snid 4633	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅}
68	66, 67	eqeltri 2862	. . . . . . . . . . . . . . 15 ⊢ ∪ {∅} ∈ {∅}
69		unieq 4888	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → ∪ 𝐴 = ∪ {∅})
70		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → 𝐴 = {∅})
71	69, 70	eleq12d 2860	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = {∅} → (∪ 𝐴 ∈ 𝐴 ↔ ∪ {∅} ∈ {∅}))
72	68, 71	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {∅} → ∪ 𝐴 ∈ 𝐴)
73	72	orim2i 924	. . . . . . . . . . . . 13 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ ∪ 𝐴 ∈ 𝐴))
74	73	ord 878	. . . . . . . . . . . 12 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
75	64, 74	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
76	63, 75	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
77	59, 76	sylbir 238	. . . . . . . . 9 ⊢ (∪ 𝐴 = ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
78	77	com12 33	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∪ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
79	78	con3d 153	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∪ 𝐴 = ∅))
80	56, 55, 79	sylc 66	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 = ∅)
81		ioran 999	. . . . . 6 ⊢ (¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅) ↔ (¬ ∪ 𝐴 ∈ 𝐴 ∧ ¬ ∪ 𝐴 = ∅))
82	55, 80, 81	sylanbrc 595	. . . . 5 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
83		uniun 4900	. . . . . . . 8 ⊢ ∪ (𝐴 ∪ {∅}) = (∪ 𝐴 ∪ ∪ {∅})
84	66	uneq2i 4122	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∪ {∅}) = (∪ 𝐴 ∪ ∅)
85		un0 4354	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∅) = ∪ 𝐴
86	83, 84, 85	3eqtri 2793	. . . . . . 7 ⊢ ∪ (𝐴 ∪ {∅}) = ∪ 𝐴
87	86	eleq1i 2857	. . . . . 6 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ∪ 𝐴 ∈ (𝐴 ∪ {∅}))
88		elun 4110	. . . . . 6 ⊢ (∪ 𝐴 ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}))
89	65	elsn2 4636	. . . . . . 7 ⊢ (∪ 𝐴 ∈ {∅} ↔ ∪ 𝐴 = ∅)
90	89	orbi2i 926	. . . . . 6 ⊢ ((∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
91	87, 88, 90	3bitri 300	. . . . 5 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
92	82, 91	sylnibr 332	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93		unieq 4888	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = ∪ (𝐴 ∪ {∅}))
94		id 23	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
95	93, 94	eleq12d 2860	. . . . 5 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
96	95	notbid 321	. . . 4 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
97	92, 96	syl5ibrcom 250	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})))
98	54, 97	mpd 16	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
99	50, 98	pm2.65da 829	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ≠ wne 2961 ∀wral 3082 {crab 3419 Vcvv 3458 ∪ cun 3906 ⊆ wss 3908 ∅c0 4289 𝒫 cpw 4567 {csn 4594 ∪ cuni 4877 class class class wbr 5114 ↦ cmpt 5197 Or wor 5573 ran crn 5667 suc csuc 6369 ⟶wf 6539 ‘cfv 6543 [⊊] crpss 7732 ωcom 7871 ≼ cdom 8950 Fincfn 8952 Fin^IIIcfin3 10283

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-rpss 7733 df-om 7872 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-wdom 9537 df-card 9944 df-fin4 10289 df-fin3 10290

This theorem is used by: fin1a2s 10416

W3C validator